Nuprl Lemma : d-m_wf
11,40
postcript
pdf
D
:Dsys,
i
:Id. M(
i
)
MsgA
latex
Definitions
x
:
A
.
B
(
x
)
,
Dsys
,
t
T
,
M(
i
)
Lemmas
Id
wf
,
msga
wf
origin
D:Dsys, i:Id. M(i) 
MsgA D:Dsys, i:Id. M(i) MsgA x:A. B(x) T